package karpiel.boguchwal.wojciech.przemek

import karpiel.boguchwal.wojciech.przemek.Ast._
import org.scalatest.FunSuite

class TypeNormalizerTest extends FunSuite {

  test("testNormalized") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty.append(Universe(0), UnitType)
    assert(Bruijn(0).normalized == UnitType)
  }

  test("sumType") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty
    assert(PiElim(SumElim(PiValue(BoolType, BoolTrue), PiValue(UnitType, BoolFalse)), SumInl(BoolFalse, UnitType)).normalized == BoolTrue)
    assert(PiElim(SumElim(PiValue(BoolType, BoolTrue), PiValue(UnitType, BoolFalse)), SumInl(BoolFalse, UnitType)).normalized == BoolTrue)
    assert(PiElim(SumElim(PiValue(BoolType, BoolTrue), PiValue(UnitType, BoolFalse)), SumInr(BoolType, UnitValue)).normalized == BoolFalse)
  }

  test("bool") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty

    def neg = BoolElim(BoolFalse, BoolTrue)

    assert(PiElim(neg, BoolTrue).normalized == BoolFalse)
    assert(PiElim(neg, BoolFalse).normalized == BoolTrue)

    val fn = PiValue(BoolType, PiElim(BoolElim(SumType(UnitType, UnitType), UnitType), Bruijn(0)))
    assert(PiElim(BoolRec(fn, SumInl(UnitValue, UnitType), UnitValue), BoolTrue).normalized == SumInl(UnitValue, UnitType))
    assert(PiElim(BoolRec(fn, SumInl(UnitValue, UnitType), UnitValue), BoolFalse).normalized == UnitValue)

    assertThrows[Exception](PiElim(
      BoolRec(PiValue(UnitType, PiElim(BoolElim(SumType(UnitType, UnitType), UnitType), Bruijn(0))),
        SumInl(UnitValue, UnitType), UnitValue), BoolTrue).normalized)
    assertThrows[Exception](PiElim(
      BoolRec(fn, SumInl(UnitValue, UnitType), BoolTrue), BoolFalse).normalized)
    assertThrows[Exception](PiElim(BoolRec(PiValue(BoolType, PiElim(BoolElim(SumType(UnitType, UnitType), Universe(0)), Bruijn(0))),
      SumInl(UnitValue, UnitType), BoolType), BoolTrue).normalized)
  }

  test("sigma") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty
    val v = SigmaValue(BoolTrue, UnitValue, PiElim(BoolElim(UnitType, BoolType), Bruijn(0)))
    val f1 = SigmaElim(PiValue(BoolType, PiValue(PiElim(BoolElim(UnitType, BoolType), Bruijn(0)), UnitType)))
    assert(PiElim(f1, v).normalized == UnitType)

    val f2 = SigmaElim(PiValue(BoolType, PiValue(PiElim(BoolElim(UnitType, BoolType), Bruijn(0)), Bruijn(0))))
    assert(PiElim(f2, v).normalized == UnitValue)
    val f3 = SigmaElim(PiValue(BoolType, PiValue(PiElim(BoolElim(UnitType, BoolType), Bruijn(0)), Bruijn(1))))
    assert(PiElim(f3, v).normalized == BoolTrue)

    val v2 = SigmaValue(BoolFalse, UnitValue, PiElim(BoolElim(UnitType, BoolType), Bruijn(0)))
    assertThrows[Exception](PiElim(f3, v2).normalized)

    assert(Proj1(v).normalized == BoolTrue)
    assert(Proj2(v).normalized == UnitValue)

  }

  test("ID") {
    implicit val cache: Cache = RealCache()
    assert(PiElim(PiElim(PiElim(
      J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, UnitValue)),
      Bruijn(0)), Bruijn(0)), Refl(Bruijn(0))).normalized(Context.Empty.append(BoolType), implicitly) == UnitValue)


    assertThrows[Exception](PiElim(PiElim(PiElim(
      J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, UnitValue)),
      Bruijn(0)), Bruijn(0)), Refl(Bruijn(0))).normalized(Context.Empty.append(UnitType), implicitly))

    //this could throw aswell
    assert(PiElim(PiElim(PiElim(
      J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, UnitValue)),
      Bruijn(0)), BoolFalse), Refl(Bruijn(0))).normalized(Context.Empty.append(BoolType, BoolTrue), implicitly) ==
      PiElim(PiElim(PiElim(J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))),
        PiValue(BoolType, UnitValue)), BoolTrue), BoolFalse), Refl(BoolTrue)))

    //this could throw aswell
    assert(PiElim(PiElim(PiElim(
      J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, UnitValue)),
      Bruijn(0)), Bruijn(0)), Refl(BoolFalse)).normalized(Context.Empty.append(BoolType, BoolTrue), implicitly) ==
      PiElim(PiElim(PiElim(J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, UnitValue)), BoolTrue), BoolTrue), Refl(BoolFalse)))


    assert(PiElim(PiElim(PiElim(
      J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, UnitValue)),
      Bruijn(0)), Bruijn(0)), Refl(BoolTrue)).normalized(Context.Empty.append(BoolType, BoolTrue), implicitly) == UnitValue)
    assert(PiElim(PiElim(PiElim(
      J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, UnitValue)),
      Bruijn(0)), BoolTrue), Refl(BoolTrue)).normalized(Context.Empty.append(BoolType, BoolTrue), implicitly) == UnitValue)
  }

  test("W") {
    import StdLib.Nat._
    implicit val cache: Cache = RealCache()
    double.normalized(Context.Empty, implicitly)
    val twoTimesone = PiElim(double, one).normalized(Context.Empty, implicitly)
    val twoTimesTwo = PiElim(double, PiElim(succ, one)).normalized(Context.Empty, implicitly)

    //2*0 = 0
    assert(PiElim(double, zero).normalized(Context.Empty, implicitly) == zero)
    //2*1 = 2
    assert(twoTimesone == PiElim(succ, one).normalized(Context.Empty, implicitly))
    //2*2 = 4
    assert(twoTimesTwo.normalized(Context.Empty, implicitly) == PiElim(succ, PiElim(succ, PiElim(succ, one))).normalized(Context.Empty, implicitly))

    // 2*1 != 1
    assert(twoTimesone != one.normalized(Context.Empty, implicitly))
    // 2 != 4
    assert(twoTimesone != twoTimesTwo)
  }
}
